Termination Proof Script
Consider the TRS R consisting of the rewrite rules
|
| 1: |
|
active(f(X)) |
→ mark(g(h(f(X)))) |
| 2: |
|
active(f(X)) |
→ f(active(X)) |
| 3: |
|
active(h(X)) |
→ h(active(X)) |
| 4: |
|
f(mark(X)) |
→ mark(f(X)) |
| 5: |
|
h(mark(X)) |
→ mark(h(X)) |
| 6: |
|
proper(f(X)) |
→ f(proper(X)) |
| 7: |
|
proper(g(X)) |
→ g(proper(X)) |
| 8: |
|
proper(h(X)) |
→ h(proper(X)) |
| 9: |
|
f(ok(X)) |
→ ok(f(X)) |
| 10: |
|
g(ok(X)) |
→ ok(g(X)) |
| 11: |
|
h(ok(X)) |
→ ok(h(X)) |
| 12: |
|
top(mark(X)) |
→ top(proper(X)) |
| 13: |
|
top(ok(X)) |
→ top(active(X)) |
|
There are 21 dependency pairs:
|
| 14: |
|
ACTIVE(f(X)) |
→ G(h(f(X))) |
| 15: |
|
ACTIVE(f(X)) |
→ H(f(X)) |
| 16: |
|
ACTIVE(f(X)) |
→ F(active(X)) |
| 17: |
|
ACTIVE(f(X)) |
→ ACTIVE(X) |
| 18: |
|
ACTIVE(h(X)) |
→ H(active(X)) |
| 19: |
|
ACTIVE(h(X)) |
→ ACTIVE(X) |
| 20: |
|
F(mark(X)) |
→ F(X) |
| 21: |
|
H(mark(X)) |
→ H(X) |
| 22: |
|
PROPER(f(X)) |
→ F(proper(X)) |
| 23: |
|
PROPER(f(X)) |
→ PROPER(X) |
| 24: |
|
PROPER(g(X)) |
→ G(proper(X)) |
| 25: |
|
PROPER(g(X)) |
→ PROPER(X) |
| 26: |
|
PROPER(h(X)) |
→ H(proper(X)) |
| 27: |
|
PROPER(h(X)) |
→ PROPER(X) |
| 28: |
|
F(ok(X)) |
→ F(X) |
| 29: |
|
G(ok(X)) |
→ G(X) |
| 30: |
|
H(ok(X)) |
→ H(X) |
| 31: |
|
TOP(mark(X)) |
→ TOP(proper(X)) |
| 32: |
|
TOP(mark(X)) |
→ PROPER(X) |
| 33: |
|
TOP(ok(X)) |
→ TOP(active(X)) |
| 34: |
|
TOP(ok(X)) |
→ ACTIVE(X) |
|
The approximated dependency graph contains 6 SCCs:
{20,28},
{29},
{21,30},
{17,19},
{23,25,27}
and {31,33}.
-
Consider the SCC {20,28}.
There are no usable rules.
By taking the AF π with
π(F) = π(mark) = 1 together with
the lexicographic path order with
empty precedence,
rule 20
is weakly decreasing and
rule 28
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {20}.
By taking the AF π with
π(F) = 1 together with
the lexicographic path order with
empty precedence,
rule 20
is strictly decreasing.
-
Consider the SCC {29}.
There are no usable rules.
By taking the AF π with
π(G) = 1 together with
the lexicographic path order with
empty precedence,
rule 29
is strictly decreasing.
-
Consider the SCC {21,30}.
There are no usable rules.
By taking the AF π with
π(H) = π(mark) = 1 together with
the lexicographic path order with
empty precedence,
rule 21
is weakly decreasing and
rule 30
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {21}.
By taking the AF π with
π(H) = 1 together with
the lexicographic path order with
empty precedence,
rule 21
is strictly decreasing.
-
Consider the SCC {17,19}.
There are no usable rules.
By taking the AF π with
π(ACTIVE) = π(f) = 1 together with
the lexicographic path order with
empty precedence,
rule 17
is weakly decreasing and
rule 19
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {17}.
By taking the AF π with
π(ACTIVE) = 1 together with
the lexicographic path order with
empty precedence,
rule 17
is strictly decreasing.
-
Consider the SCC {23,25,27}.
There are no usable rules.
By taking the AF π with
π(f) = π(g) = π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
the rules in {23,25}
are weakly decreasing and
rule 27
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {23,25}.
By taking the AF π with
π(f) = π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 23
is weakly decreasing and
rule 25
is strictly decreasing.
There is one new SCC.
-
Consider the SCC {23}.
By taking the AF π with
π(PROPER) = 1 together with
the lexicographic path order with
empty precedence,
rule 23
is strictly decreasing.
-
Consider the SCC {31,33}.
The usable rules are {1-11}.
By taking the AF π with
π(f) = π(g) = π(h) = π(TOP) = 1
and π(active) = π(mark) = π(ok) = π(proper) = [ ] together with
the lexicographic path order with
precedence ok ≻ active ≻ mark ≻ proper,
the rules in {2-11}
are weakly decreasing and
the rules in {1,31,33}
are strictly decreasing.
Hence the TRS is terminating.
Tyrolean Termination Tool (0.25 seconds)
--- May 4, 2006